A, B:Type, opa:(AAA), opb:(BBB), f:(AB).
Inj(A;B;f)  FunThru2op(A;B;opa;opb;f)  Comm(B;opb)  Comm(A;opa) 

latex

Up	gen algebra 1
Definitions of Statement	Comm(T;op), FunThru2op(A;B;opa;opb;f)
Definitions	t  T, Comm(T;op), P  Q, x:A. B(x), P & Q, P  Q, P  Q, x f y, FunThru2op(A;B;opa;opb;f), Inj(A;B;f),
Lemmas	inject wf, fun thru 2op wf, comm wf